%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newpage
\iflong{\section{Axiomatization and Complexity}\label{s:axiom}}{\Section{Axiomatization and Complexity}\label{s:axiom}}

We have shown in the previous section that the main forms
of bisimilarity for higher-order process calculi coincide in \ahopi. 
%In this section w
We therefore simply call \emph{bisimilarity} such a
relation, and write it as $\sim$.
Here
%In this section 
we present a sound and complete axiomatization 
of bisimilarity. We do so by adapting to a higher-order setting results by Moller and Milner on 
unique decomposition of processes \citep{MM93,Moller88}, and by 
Hirschkoff and Pous on an axiomatization for a fragment of (finite) CCS \citep{Hir07}.
We then exploit this axiomatization 
%his result 
to derive complexity bounds for bisimilarity checking.
% We obtain this by adapting results of Milner and Moller \cite{..} and
% Hirskhoff and Pous \cite{..} from pure CCS  to our higher-order
% setting. 

\iflong{\subsection{Axiomatization}}{}


\begin{lemma}\label{lemma:size}
$P \sim Q$ implies $\size{P}=\size{Q}$.
\end{lemma}
\iflong{
\begin{proof}
Suppose, for a contradiction, that there exist $P,Q$ such that $P \sim Q$ with $\size{P} < \size{Q}$
and choose a $P$ with a minimal size. If $Q$ has no transition enabled, then it must be $\nil$, thus $\size{Q} = 0$, which is impossible as $\size{Q} > \size{P} \geq 0$.

We thus have $Q \arr \alpha Q'$, hence there is a $P'$ such that $P  \arr \alpha P'$ with $P' \sim Q'$. We consider two cases, depending on the shape of $\alpha$ (we do not consider $\tau$ actions, as such an action implies both an input and an output).

If $\alpha$ is an input action, we have $Q \arr{a(x)} Q'$, and since $P \sim Q$, then also $P  \arr{a(x)} P'$. 
We then have that $\size{P'} = \size{P}-1$ and $\size{Q'} = \size{Q}-1$, so it follows that $\size{P'} < \size{Q'}$. 
Further, one has $\size{P'} < \size{P}$, which contradicts the minimality hypothesis.

Now suppose $\alpha$ is an output action: we have $Q \arr{\out a {Q''}} Q'$, and by definition of $\sim$, also 
that $P \arr{\out a {P''}} P'$ with both $P' \sim Q'$ and $P'' \sim Q''$. By the definition of size, we have that 
$\size{P'} = \size{P} - (1 + \size{P''})$ and $\size{Q'} = \size{Q} - (1 + \size{Q''})$. 
Notice that $P''$, $Q''$ are strict subterms of $P$ and $Q$, respectively. If their size is not the same, we have a contradiction. Otherwise, we have $\size{P'} < \size{Q'}$ and also $\size{P'} < \size{P}$, which is also a contradiction.
\end{proof}}{}




Following %Moller and Milner 
\citep{MM93,Moller88} we prove   
a result of unique  prime decomposition of processes. %  and a derived  cancellation property.

\begin{mydefi}[Prime decomposition]
A process $P$ is {\em prime} if $P \not \sim \nil$ and $P \sim P_1
\parallel P_2$ imply $P_1 \sim \nil$ or $P_2 \sim \nil$. When $P \sim \prod_{i=1}^{n} P_i$ where each $P_i$ is prime, 
we call $\prod_{i=1}^{n} P_i$ a {\em prime decomposition} of $P$.
\end{mydefi}

\begin{myprop}[Cancellation]\label{coro:canc}
For all $P$, $Q$,  and  $R$, if $P \parallel R \sim Q \parallel R$
then also
$P \sim Q$.
\end{myprop}
\begin{proof}
The proof, which proceeds by induction on $\size{P}+\size{Q}+\size{R}$, is a simple adaptation of the one in \citep{MM93}.
\end{proof}

\begin{myprop}[Unique decomposition]
\label{p:ud}
Any process $P$ admits a prime decomposition 
%$P_1 \parallel \dots \parallel P_n$ 
$\prod_{i=1}^{n} P_i$
which is unique up to bisimilarity and permutation of indices (i.e.,
 given two prime decompositions $\prod_{i=1}^{n} P_i$ and $\prod_{i=1}^{m} P'_i$, then $n = m$ and 
there is a permutation $\sigma$ of $\{1,\dots,n\}$ such that $P_i \sim P'_{\sigma(i)}$ for each $i \in \{1,\dots,n\}$).
\end{myprop}
\iflong{
 \begin{proof}
The proof, also similar to the one in \citep{MM93} with just variables to  be considered in addition, uses Proposition \ref{coro:canc}.
 \end{proof}}{}


  
Both the key law for the axiomatization and the following results are inspired 
by similar ones by  \cite{Hir07} for pure CCS. 
Using their terminology, we call \emph{distribution law}, briefly (\DIS),
the axiom schema below
\iflong{(recall that $\prod_{1}^{k}  Q$ denotes the parallel composition of $k$ copies of $Q$).}{
($\prod_{1}^{k}  Q$ denotes the parallel composition of $k$ copies of $Q$.)}

\begin{center}
$ $ \hfill 
$ a(x).(P \parallel \prod_{1}^{k-1}{a(x).P}) \: = \;
\prod_{1}^{k} {a(x).P }
$ \hfill (\DIS)
\end{center} 

We then call \emph{extended structural congruence}, written $\ext$,
 the extension of the 
structural congruence relation ($\equiv $, Definition~\ref{d:struct}) with
the axiom schema  (\DIS). 
\iflong{
We write $P \rewrite Q$ when there are processes $P'$ and
 $Q'$ such that $P \equiv P'$, $Q' \equiv Q$ and $Q'$ is obtained from
 $P'$ by rewriting a subterm of $P'$ using  law (\DIS)  from left to right.
Below we prove that $\ext$ provides an algebraic  characterization  of
$\sim$ in \ahopi. 
Establishing the soundness of $\ext$ is easy;  below we discuss 
completeness. 

\begin{mydefi}
A process $P$ is in \emph{normal form} if it cannot be further
simplified in the system $\ext$  by 
%applications of  law (\DIS) from left to right.
using $\rewrite.$
\end{mydefi}
}{
Below we prove that $\ext$ gives us an algebraic  characterization  of
$\sim$ in \ahopi. 
Establishing the soundness of $\ext$ is easy;  below we discuss 
completeness. 

A process $P$ is in \emph{normal form} if it cannot be further
simplified in the system $\ext$  by applications of  law (\DIS) from
left to right. 
Formally,  there 
are no processes $P'$ and  $Q'$ such that $P \equiv P'$, 
%$Q' \equiv Q$ 
and $Q'$ is obtained from the 
%$P'$ by 
rewriting of a  subterm of $P'$
%is no process $P'$ obtained from rewriting a subterm of $P$
using law (\DIS) from left to right.}
Any process $P $ 
has 
a normal form that is 
unique up to $\equiv$, and which
will be  denoted by $\nf{P}$.
Below $A$ and 
 $B$ range over normal forms, and 
 a process is 
said to be 
\emph{non-trivial} if its size is %different from 
not 0. 



\iflong{
\begin{lemma}\label{lemma:nfbisim}
If $P \rewrite Q$, then $P \sim Q$. Also, for any $P$, $P \sim \nf{P}$.
\end{lemma}
\begin{proof}
The proof proceeds 
%Straightforward 
%from the definitions of $\sim$ (as $\simIOo$, for instance), \DIS\ and its associated normal form.
by showing that $(\rewrite \cup \,(\rewrite)^{-1}\, \cup \equiv)$ is a bisimulation (as $\simIOo$, for instance).
\end{proof}
}{}

%\begin{mycoro}[Cancellation]\label{coro:canc}
%For all $P$, $Q$, $R$, $P \parallel R \simIOo Q \parallel R$ implies
%$P \simIOo Q$.
%\end{mycoro}

\begin{lemma}\label{lemma:prefdec}
If $a(x).P \sim Q \parallel Q'$ with $Q, Q' \not \sim \nil$,
then  $a(x).P \sim
\prod_{1}^{k}\, {a(x).A}$, where $k> 1$ and 
 $a(x).A$ is in normal form.
\end{lemma}
\iflong{
\begin{proof}
%\iflong{
By Lemma~\ref{lemma:nfbisim}, $a(x).P \sim \nf{Q \parallel
Q'}$. Furthermore,  by Proposition~\ref{p:ud}, we have that 
$$
\nf{Q \parallel Q'} \equiv \prod_{i\leq k} a_i(x_i).A_i \parallel \prod_{j \leq l} \out {b_j}{B_j} ,
$$ 
where the processes $a_i(x_i).A_i$ and $\out {b_j}{B_j}$ are in normal form and prime. 
Since the prefix $a(x)$ must be triggered to answer any challenge from the right-hand side, we have $a_i=a$, and $x_i=x$ (this can be obtained via $\alpha$-conversion, but we can suppose that $a_i(x_i).A_i$ was already $\alpha$-converted to the correct form), and we have $l = 0$ (there is no output in the prime decomposition). As there are at least two processes that are not $\nil$, we have $k > 1$. To summarize:
\[
  a(x).P \sim \prod_{i\leq k} a(x).A_i.
\]
After an input action on the right-hand side, we derive
$$
P \sim A_i \parallel \prod_{l \neq i} a(x).A_l
$$ 
for every $i \leq k$. In particular, when $i \neq j$, we have 
$$P \sim A_i \parallel a(x).A_j \parallel \prod_{l \notin \{i,j\}} a(x).A_l \quad \quad P \sim  A_j \parallel a(x).A_i \parallel \prod_{l \notin \{i,j\}} a(x).A_l$$ 
and, by Proposition~\ref{coro:canc}, $A_i \parallel a(x).A_j \sim A_j \parallel a(x).A_i$. Since $a(x).A_i$ is prime and it has larger size than $A_i$ (and any of its components), it should correspond in the prime decomposition to $a(x).A_j$, i.e. $a(x).A_i \sim a(x).A_j$. As this was shown for every $i \neq j$, we thus have $a(x).P \sim \prod^k_1 a(x).A_1$ with $k>1$ and $a(x).A_1$
in normal form.
%}{The proof is similar to the one in \cite{MM93}.}
\end{proof}
}{
The proof of Lemma \ref{lemma:prefdec} exploits Proposition \ref{p:ud} and Corollary \ref{coro:canc}.
}




\begin{lemma}\label{l:nfequiv}
For $A,B$ in normal form, if $A \sim B$ then $A \equiv B$.
\end{lemma}
\iflong{
\begin{proof}[Proof]
%We show by induction on $n$ that for all $A$ with $\size{A}=n$, we have:
We show, simultaneously, the following two properties:
\begin{enumerate}
\item if $A$ is a prefixed process in normal form, then $A$ is prime;
\item for any $B$ in normal form, $A \sim B$ implies $A \equiv B$.
\end{enumerate}
We proceed by induction on $n$, for all $A$ with $\size{A}=n$.
The case $n=0$ is immediate as the only process of this size is $\nil$. 
Suppose that the property holds for all $i<n$, with $n \geq 1$.
In the reasoning below, we exploit the characterization of $\sim$ as $\simIOo$.
\begin{enumerate}

%Jorge's version
\item Process  $A$ is of the form $ a(x).A'$. Suppose, as a contradiction, that $A$ is not prime. 
Then we have $A \sim P_1 \parallel P_2$ with $P_1$ and $P_2$ non-trivial. 
By Lemma~\ref{lemma:prefdec}, then $A \sim \Bigpi 1 k {a(x).B}$ with
$k>1$ and $a(x).B$ in normal form. By consuming the prefix on the
left-hand side, we have $A' \sim B \parallel \Bigpi 1{k-1}{a(x).B}$. It
follows by induction (using property (2)) that $A' \equiv B \parallel \Bigpi 1{k-1}{a(x).B}$, 
and hence also  $A \equiv a(x).(B \parallel \Bigpi 1 {k-1} {a(x).B})$. 
This is impossible, as  $A$ is in normal form. 

\item Suppose $A \sim B$. We proceed by case analysis on the structure of $A$.
\begin{itemize}

\item Case $A = x$. We have that $B$ should be the same variable, so $A \equiv B$ trivially.
\item Case $A = \out a P$. We have that $B = \out a {P'}$ with $P \sim P'$ by definition of $\simIOo$. 
      By the induction hypothesis, $P \equiv P'$, thus $\out a P \equiv  \out a {P'}$.

\item Case $A =  a(x).A'$. We show by contradiction that 
  $B = a(x).B'$. Assume $B = Q \parallel Q'$, then by Lemma \ref{lemma:prefdec}, $A$ is a parallel composition of at least two processes. But according to the first property, as $A$ is prefixed, it is prime, a contradiction. We thus have $B = a(x).B'$ with $A' \simIOo B'$. By
  induction this entails $A' \equiv B'$ and $A \equiv B$.


\item Case $A =\prod_{i \leq k} P_i$ with $k>1$ where no $P_i$ has a 
parallel composition at top-level. We reason on the possible shape of the $P_i$.

If there exists $j$ such that $P_j=x$ 
then also $B \equiv x \parallel B'$. The thesis then follows by induction
hypothesis on $\prod_{i \leq k, i \neq j} P_i$ and $B'$. 

If $P_i$ is an output, $B$ must contain an output on the same channel.
The thesis then follows by applying the induction hypothesis twice, to the arguments and to the 
other parallel components. 

The last case is when    
$A \equiv \prod_{i \leq k} a_i(x_i).A_i$ with $k>1$.
We know by the induction hypothesis (property (1)) that each component $a_i(x_i).A_i$ is prime.
Similarly, it must be $B \equiv \prod_{i \leq l} b_i(x_i).B_i$ with $b_i(x_i).B_i$ prime for all $i \leq 
l$. By Proposition~\ref{p:ud} (unique decomposition), we infer $k=l$ and $a_i(x_i).A_i 
\sim b_i(x_i).B_i$ (up to a permutation of indices). Thus $a_i = b_i$ and $A_i 
\sim B_i$; then by induction $A_i \equiv B_i$ for all $i$, which 
finally implies $A \equiv B$. 
\end{itemize}
\end{enumerate}
\end{proof}
}{ %%% end iflong
The proof of Lemma \ref{l:nfequiv} is similar 
 to the one in \citep{Hir07}, with some extra cases. 
}
The theorem below follows\iflong{ from Lemmas \ref{lemma:nfbisim} and \ref{l:nfequiv}.}{.}

\begin{mytheo}
For any processes $P$ and $Q$, we have 
 $P \sim Q$ iff $\nf{P} \equiv \nf{Q}$.
\end{mytheo}

\begin{corollary}
$\ext$ is a sound and complete axiomatization of bisimilarity  in \ahopi.
\end{corollary} 

\iflong{\subsection{Complexity of Bisimilarity Checking}}{}
To analyze
the complexity of deciding whether two processes are
bisimilar, one could apply the technique from \citep{DovierPP04},
and derive that 
%which allows to decide 
bisimilarity is decidable in time which is linear in the size of the
LTS for $\simIOo$ (which avoids $\tau$ transitions). This LTS is however exponential in the size of the process.
A more efficient solution exploits the axiomatization above: one can
normalize processes
%\iflong{}{, described in Appendix \ref{a:axiom}}, 
and reduce bisimilarity to syntactic equivalence
of normal forms.

\iflong
{For simplicity,  we assume a process $P$ is represented as an ordered
tree (but we will transform it into a DAG during normalization).
In the following, let us denote with $t [m_1, \ldots, m_k]$ the ordered tree with root labeled $t$ and with 
(ordered) descendants $m_1, \ldots, m_k$. We write $t[]$ for a tree labeled $t$ and without descendants (i.e., a leaf).

\begin{mydefi}[Tree representation]\label{d:tree}
Let $P$ be a \ahopi process. Its associated ordered tree representation is labeled and 
defined inductively by
\begin{itemize}
\item $\mathsf{Tree}(\nil) = \nil[]$
\item $\mathsf{Tree}(x) = \mathsf{db}(x)[]$
\item $\mathsf{Tree}(\out a {Q}) = \bar{a} [\mathsf{Tree}(Q)]$
\item $\mathsf{Tree}(a(x).Q) = a[\mathsf{Tree}(Q)]$ 
\item $\mathsf{Tree}(\prod_{i=1}^n P_i) = \prod_{i=1}^n [\mathsf{Tree}(P_1),\ldots,\mathsf{Tree}(P_n)]$ 
\end{itemize}
where $\mathsf{db}$ is a function assigning De Bruijn indices \cite{db} to variables. 
\end{mydefi}



We now describe the normalization steps. 
The first deals with parallel composition nodes: it removes all unnecessary $\nil$ nodes, and 
relabels the nodes when the parallel composition has only one or no descendants.   

\begin{norm}\label{norm:nil}
Let $\rewrite_{\mathtt{N1}}$ be a transformation rule over trees associated to \ahopi processes, defined by:

\begin{enumerate}
\item $\prod_{i={1}}^n [\mathsf{Tree}(P_{1}),\ldots,\mathsf{Tree}(P_{n})]  \rewrite_{\mathtt{N1}} \prod_{i=1}^{m} [\mathsf{Tree}(P_{\sigma(1)}), \ldots, \mathsf{Tree}(P_{\sigma(m)})]$, \\
where $m < n$ is the number of processes in $P_1, \ldots, P_n$ that are different from $\nil$, 
and  $\sigma$ is a bijective function from $\{1,\ldots,m\}$ to $ \{ i \,|\, i \in \{1,\ldots, n\} \land P_i \not = \nil \}$.
\item $\prod_{i=1}^0  [] \rewrite_{\mathtt{N1}} \nil[] $
\item $\prod_{i=1}^1 [\mathsf{Tree}(P_1)]   \rewrite_{\mathtt{N1}} \mathsf{Tree}(P_1) $
\end{enumerate}
\end{norm}

After this first step, the tree is traversed bottom-up, applying the
following normalization steps.

\begin{norm}\label{norm:sort}
Let $\rewrite_{\mathtt{N2}}$ be a transformation rule over trees associated to \ahopi processes, defined as follows.
If the node is a parallel composition, sort all the children
lexicographically. If $n$ children are equal, leave just one and make
$n$ references to it.
\end{norm}

The last step applies \DIS\ from left to right if possible.
\begin{norm}\label{norm:rewrite}
Let $\rewrite_{\mathtt{N3}}$ be a transformation rule over trees associated to \ahopi processes, defined by:
%\begin{itemize}
%\item $
\begin{eqnarray*}
a\,\left[\,\prod_{i={1}}^{k+1}[\mathsf{Tree}(P), \mathsf{Tree}( a(x).P), \ldots, \mathsf{Tree}( a(x).P)]\right]  \rewrite_{\mathtt{N3}} \\
\quad \prod_{j=1}^{k+1} [\mathsf{Tree}(a(x).P),\ldots,\mathsf{Tree}(a(x).P)]
\end{eqnarray*}
where %, in product in the left-hand side, 
$\mathsf{Tree}( a(x).P)$ appears $k$ times in the left-hand side, and $k+1$ times in the right-hand side.
%\end{itemize}
\end{norm}

%\iflong{
Notice that applying \DIS\ changes De Bruijn indices, but the first
instance of $P$ already has the correct indices, thus making $n$
references to it produces the correct DAG.
Note also that in the comparison between the different instances of $P$, care
should be taken because of the  De Bruijn indices. 
In fact, De Bruijn indices 
of all the instances of $P$ but the first one 
%greater than that of $x$ 
are increased by one, since there is one more binding occurrence of $x$.

%The check requires to compare trees for structural congruence, but the
%lemma below shows that comparing for syntactic identity is enough (to
%be precise De Bruijn indices of the second component but $1$ should be
%decreased by $1$ for the comparison).

\begin{lemma}\label{l:nsts12}
Let $T_P,T_Q$ be two tree representations of processes $P$ and $Q$
(as in Definition \ref{d:tree}), 
normalized according to normalization steps \ref{norm:nil} and
\ref{norm:sort}. Then $P \equiv Q$ iff $T_P=T_Q$.
\end{lemma}

\begin{proof}
Immediate from Definitions \ref{d:struct} and \ref{d:tree}, and from normalization steps 1 and 2.
In particular, $\rewrite_{\mathtt{N1}}$ 
corresponds to the elimination of all occurrences of $\nil$ in parallel, and 
$\rewrite_{\mathtt{N2}}$ corresponds to the choice of a representative process, up to associativity and
commutativity.
%ensures that $P \parallel \nil$ and $P$  have the same tree representation, and sorting in 
%normalization step 2 can be done since $P \parallel Q \equiv Q \parallel P$. 
\end{proof}

%}{}

\begin{lemma}
Let $P,Q$ be processes and $T_P,T_Q$ their tree representations
normalized according to steps \ref{norm:nil}, \ref{norm:sort} and
\ref{norm:rewrite}. Then $P \sim Q$ iff $T_P=T_Q$.
\end{lemma}
\begin{proof}
Immediate using Lemmas \ref{l:nsts12} and \ref{lemma:nfbisim} ($P \rewrite Q$ implies $P \sim Q$).
\end{proof}

We now give a lemma on the cost of sorting the tree representation of a process. 
Given a process $P$, we define the size of its tree representation $T_P$ to be 
the number of nodes of the tree, and denote it as $\sizet{P}$.

\begin{lemma}\label{l:sort}
Consider $n$ \ahopi processes $P_1, \ldots, P_n$ and their 
tree representations $T_{P_1}, \ldots, T_{P_n}$. Their sorting has complexity $O(t\, \log n)$, where
$t = \sum_{i \in 1..n} \sizet{P_i}$.
\end{lemma}
\begin{proof}
Let us assume \textsc{MergeSort} as sorting algorithm. \textsc{MergeSort} sorts a list of elements by
(i) splitting the list to be sorted in two; (ii) recursing on both sublists; and (iii) merging the sorted sublists.
A merge function starts by comparing the first element of each list
and then copies the smallest one to the new list. 
Comparing two elements $P_i,P_j$ %has a constant cost (i.e. it is a pointer operation). 
%Notice that comparing $T_{P_i}$ and $T_{P_j}$ 
costs $\min{(\sizet{P_i},\sizet{P_j})}$. 
%; hence
%the cost of copying the smallest element to the new list is equal to its size. 
%Note that we assume that comparing two elements has a much bigger cost than moving/changing a reference in memory (i.e. a pointer operation). 
As each $T_{P_i}$ is considered once (when it is copied to the new list) the cost of merging two lists is 
the sum of the size of their elements (the actual copying of an element has constant cost since it is just
a pointer operation).
Let us call a {\em slice} of \textsc{MergeSort} the juxtaposition of every recursive call at the same depth. In this way, e.g., 
the first slice considers the lists when recursion depth is equal to 1: 
the first two recursive calls, each one having half of the original list. 
In general, at every slice one finds a partition of the list in $2^d$ sublists, where $d$ is the recursion depth.
Each recursive call in every slice is going to merge two sublists, with a complexity of the sum of the sizes of these sublists.
Summing everything, we get a cost of $t = \sum_{i \in 1..n} \sizet{P_i}$ at each recursion depth. Therefore, as there are
$\log n$ different depths, the total complexity is $O(t \log n)$.
\end{proof}
}{
%%% Short normalization procedure
For simplicity, we assume a process is represented as an ordered
tree (but we will transform it into a DAG during normalization), with
variables represented by De Bruijn indices. The tree has nodes for
$\nil$, variables in De Bruijn notation, input prefixes (with the
continuation as only child), output (with the argument as only child),
and parallel composition. In particular, each node for parallel
composition has $m$ leaves, where $m$ is the number of parallel
components (none of them containing top-level parallel
compositions).

The first step of normalization is the following.

\begin{norm}\label{norm:nil}
Remove all $\nil$ nodes that are children of a parallel composition node.
Subsequently, if the parallel composition has $0$ child, replace it with $\nil$, if it has $1$ child, replace it with the child.
\end{norm}

After this first step, the tree is traversed bottom-up, applying the
following normalization steps.

\begin{norm}\label{norm:sort}
If the node is a parallel composition, sort all the children
lexicographically. If $n$ children are equal, leave just one and make
$n$ references to it.
\end{norm}

\begin{norm}\label{norm:rewrite}
If the node is an input prefix, apply \DIS\  from left to right if
possible.
\end{norm}

\iflong{
Notice that applying rewrite changes De Bruijn indices, but the first
instance of $P$ already has the correct indices, thus making $n$
references to it produces the correct DAG.

The check requires to compare trees for structural congruence, but the
lemma below shows that comparing for syntactic identity is enough (to
be precise De Bruijn indices of the second component but $1$ should be
decreased by $1$ for the comparison).

\begin{lemma}
Let $T_P,T_Q$ be two tree representations of processes $P$ and $Q$
normalized according to normalization steps \ref{norm:nil} and
\ref{norm:sort}. Then $P \equiv Q$ iff $T_P=T_Q$.
\end{lemma}}{}

\begin{lemma}
Let $P,Q$ be processes and $T_P,T_Q$ their tree representations
normalized according to steps \ref{norm:nil}, \ref{norm:sort} and
\ref{norm:rewrite}. Then $P \sim Q$ iff $T_P=T_Q$.
\end{lemma}

}


\iflong{
\begin{mytheo}
Consider two \ahopi processes $P$ and $Q$.
$P \sim Q$ can be decided in time $O(n^2 \log m)$ where 
$n=\max{(\sizet{P},\sizet{Q})}$ 
(i.e., the maximum number of nodes in the tree representations of $P$ and $Q$)
 and $m$ is the maximum branching factor in them (i.e., the maximum number of
components in a parallel composition).
\end{mytheo}
\begin{proof}
Bisimilarity check proceeds as follows: first normalize the tree
representations of the two processes, then check them for syntactic equality. 


Normalization step \ref{norm:nil} can be performed in time $O(n)$. 
%Then there are $O(n)$ steps corresponding to the second visit.
In fact, a visit ($O(n)$) is enough to apply the first rule where needed, and a second visit is enough to apply the other
two rules. Normalization step \ref{norm:sort} should be applied
if the node is a parallel composition.
By Lemma \ref{l:sort} this can be done in 
$O(n\log m)$ for each parallel composition node.  
Normalization step \ref{norm:rewrite} should be applied if the node is a prefix node. 
The check for applicability requires one comparison ($O(n)$) and the check that all
the other components coincide (simply check that the subtrees have
been merged by Normalization step 2: $O(n)$). Applying $\rewrite_{\mathtt{N3}}$ simply entails 
collapsing the trees ($O(n)$). Other nodes require no operations.

Thus
the normalization for a single node can be done in $O(n \log m)$, and the
whole normalization can be done in $O(n^2 \log m)$.
\end{proof}
}{
\begin{mytheo}
$P \sim Q$ can be decided in $O(n^2 \log m)$ where 
$n$ is the 
maximum between the 
number of nodes in the tree representations of $P$ and of $Q$, and
$m$ is the 
maximum  branching factor (i.e., the  
number of parallel components) in them.
\end{mytheo}
\begin{proof}
The most expensive part of the bisimilarity check is normalization step \ref{norm:sort}.
In particular, $O(n)$ nodes may require to apply normalization step \ref{norm:sort}, 
which requires time $O(n\log m)$ (considering that the cost of a comparison is linear in the minimum size of the compared subtrees).   
\end{proof}
}


%\subsection{Relation with synchronous calculus (less easy techniques, notably congruence  -- TO DO)}


\newcommand{\encl}[3]{\os #1,#2 \cs_{#3}}
\newcommand{\encs}[3]{\os #1,#2 \cs_{#3}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%\section{Undecidability  of bisimilarity with  four static restrictions}


\iflong{\section{Bisimilarity is Undecidable with  Four Static Restrictions}\label{s:static}}{\Section{Bisimilarity is Undecidable with  Four Static Restrictions}\label{s:static}} 

If the restriction operator is added to \ahopi, as in Plain CHOCS or
Higher-Order $\pi$-calculus,
then  recursion can be encoded \citep{Tho90,SaWabook}
and most of the results in Sections~\ref{s:bism}-\ref{s:axiom}  would break. 
In particular, higher-order 
%bisimilarity 
and context bisimilarities are
different and %are 
both undecidable \citep{San923,San96H}. 
%and 
%a clause for $\tau$-actions  in bisimilarities is necessary.


We discuss here the addition of a limited form of restriction, which
we call \emph{static restriction}. These restrictions
may not appear inside output messages: in any output  $\out a P$,
$P$ is restriction-free. 
This limitation is important: it prevents for instance the 
above-mentioned encoding of recursion from being written. 
Static restrictions could also be defined as top-level restrictions
since, by means of standard structural congruence laws,  any static restriction can be pulled out  
 at the top-level. 
%  is introduced, with the standard semantics from
% higher-order $\pi$ \cite{San923}, most of the results above break.  It
% is clear, e.g., that all $\tau$-bisimilarities are undecidable in
% \ahopi with full restriction, since e.g. one can close all channels
% and reduce termination to $\tau$-bisimilarity with a process
% performing an infinite sequence of $\tau$ actions. 
%  \finish{Cambiare in ``subsumes CCS''?}
% Here however we
% allow only a small number of static (i.e., top-level) restrictions: 
Thus the processes would take the form  $\res{a_1} \dots\res{a_n}  P$,
where $\res{a_i}$ indicates the restriction on the name $a_i$, and 
 where restriction cannot appear inside $P$ itself. 
\iflong{The operational semantics---LTS and
bisimilarities---are extended as expected. For instance, one would have 
%a rule \textsc{SrOut} that extends rule \textsc{Out} with a side condition on the emitted process. 
%One also would have 
bounded outputs as actions, as well as rules
\infrule{\textsc{StRes}~~}{P \arr\alpha P' \andalso z \not \in \fn{\alpha}}{\nu z P \arr\alpha \nu z P'}
\infrule{\textsc{StOpen}~~}{P \arr{\out a R}  P' \andalso z \in \fn{R}}{\nu z P \arr{\nu z\, {\out a R}}  P'}
defining static restriction and extrusion of restricted names, respectively. Note that there is no need to define how a bounded output interacts with input as every $\tau$ transition takes place under the restrictions.
Also, structural congruence (Definition \ref{d:struct}) would be extended with 
the axioms for restriction $\nu z \, \nu w P \equiv \nu w \, \nu z P$ and $\nu z \nil \equiv \nil$.
(In contrast, notice that we do not require the axiom: 
$\nu z (P \parallel Q) \equiv P \parallel (\nu z Q )$, where $z$ does not occur in $P$.)
We sometimes write $\nu a_1,\ldots, a_n$ to stand for $\nu a_1, \ldots, \nu a_n$.
}{(The operational semantics---LTS and
bisimilarities---are extended as expected; we omit them.) % for lack of space.)
}

We show that 
\emph{four} static restrictions are enough to make  
 undecidable
any
bisimilarity that has  little more than a  clause for $\tau$-actions. 
For this,  we reduce %proceed by a reduction of such a  problem from 
the Post correspondence problem (PCP) %There is no 's after Post (checked on wikipedia) 
\citep{Post46,Sipser05} to the bisimilarity of some processes.
%\finish{maybe also a reference from a modern textbook} 
We call 
\emph{complete $\tau$-bisimilarity} any complete 
combination of the \ahopi\ bisimulation clauses
(as defined in Section~\ref{s:bism}) that includes the clause for $\tau$
actions
(Definition~\ref{d:cla_op}(1));  the bisimilarity can
even be asynchronous (Section~\ref{s:barbed}).

% If restriction is introduced, with the standard semantics from
% higher-order $\pi$ \cite{San923}, most of the results above break.  It
% is clear, e.g., that all $\tau$-bisimilarities are undecidable in
% \ahopi with full restriction, since e.g. one can close all channels
% and reduce termination to $\tau$-bisimilarity with a process
% performing an infinite sequence of $\tau$ actions. 
% \finish{Cambiare in ``subsumes CCS''?}
% Here however we
% allow only a small number of static (i.e., top-level) restrictions: we
% consider processes of the form $\nu v_1,\dots,v_n \ P$ where $P$ does not
% contain restrictions. This is less powerful, since in particular, it
% disallows restrictions inside messages and forbids to encode
% replication of processes with restrictions (see
% Definition~\ref{defin:grepl}). The main result of this section is that
% even if $n \leq 4$, all complete
% $\tau$-bisimilarities are still undecidable, and the same holds for
% barbed congruence (note that $\simIOo$ is no longer meaningful in
% presence of restriction). To this end we reduce the problem of
% deciding any complete $\tau$-bisimilarity to Post's Correspondence Problem (PCP)
% \cite{Post46}. Thus in this section we will use $\sim$ to denote any complete $\tau$-bisimilarity.

\begin{mydefi}[PCP]
An \emph{instance} of PCP consists of an alphabet $A$ containing at
least two symbols, and a finite list $T_1,\dots,T_n$ of tiles, where
each tile is a pair of words over $A$. 
%We denote the upper word of $T_i$ as $u_i$ and the lower word as $l_i$, i.e. $T_i=(u_i,l_i)$.  
We use $T_i=(u_i,l_i)$ to denote a tile $T_i$ with upper word $u_i$ and lower word $l_i$.
A solution to this instance is a non-empty sequence of indices
$i_1,\dots,i_k$, $1 \leq i_j \leq n$ $(j \in 1 \cdots k)$, such that $u_{i_1}
\cdots u_{i_k} = l_{i_1} \cdots l_{i_k}$.  The decision problem is then
to determine whether such a solution exists or not.
\end{mydefi}


%The reason why in the paper we need to provide encodings of two
%universal machines, Minsky Machines and PCP, is that 
%the  encodings are tailored to analyzing different problems:
%undecidability of termination, and undecidability of bisimilarity  with four
%static restrictions. The PCP encoding is always
%divergent, and therefore cannot be used to reason about termination.
%On the other hand, the  MM encoding would require at least one restriction for
%each instruction of the machine.
% Also, we think that both encodings are interesting, since
%they show different ways to exploit higher-order communications for
%modeling. 

Having (static) restrictions, we refine the encoding  of
non-nested replications (Definition~\ref{defin:grepl}) and define it in the unguarded case: 
$$
\encp{!P}{!} = \res c ( Q_c \parallel \co{c}\langle Q_c \rangle)
$$ 
where $Q_c = c(x) .(x \parallel \co{c}\langle x \rangle \parallel P)$
and $P$ is a  \ahopi\  process (i.e., it is restriction-free).
In what follows we thus also consider {\em extended} \ahopi processes, that include replication and for
which structural congruence (Definition \ref{d:struct}) is extended with the axiom 
$!P \equiv P \parallel !P$.

%We assume structural congruence is extended with the axiom $!P \equiv P \parallel !P$.
%\finish{DS above: restriction was non-static, according the previous
%  definition
%To make sense of this ( and similar things in the rest of the section)
%i changed the def of static restrictions}  

% In the encoding we will use the standard encoding of unguarded replication \cite{Tho90}:
% $$
% \encp{!P}{!} = \nu m \ Y_m \parallel \co{m}\langle Y_m \rangle
% $$ 
% where $Y_m = m(X) .(X \parallel \co{m}\langle X \rangle \parallel P)$
% and $\encp{\cdot}{!}$ is an homomorphism for the other process
% constructs in \ahopi with restriction.

\iflong{
\begin{mylem}[Correctness of $\encp{\cdot}{!}$]
For each extended \ahopi process $P$: %We then have that there exists a $P'$ such that 
\begin{itemize}
\item if $\encp{P}{!}  \xrightarrow{~\alpha~} Q$ then $\exists P'$ such that either $ P \xrightarrow{~\alpha~} P'$ and
$\encp{P'}{!} = Q$ or $\alpha=\tau$, $P \equiv P'$ and $\encp{P'}{!}=Q$.
\item $P \xrightarrow{~\alpha~} P'$ implies either $\encp{P}{!} \xrightarrow{~\alpha~} \encp{P'}{!}$ or
$\encp{P}{!} \xrightarrow{~\tau~}\xrightarrow{~\alpha~} \encp{P'}{!}$. 
\end{itemize}
\end{mylem}
}

\begin{proof}
By transition induction.
\end{proof}
% {
% Notice that the encoding introduces a $\tau$ transition for each unfolding of the replication.
% }
% Notice also that the encoding exploits one top-level restriction for each
% replication (infinitely many restrictions are necessary to model
% nested replications, but we will not need this).

Now, $\encp{!\nil}{!}$ is  a purely divergent process, as it can only make
$\tau$-transitions, indefinitely; %and 
it is written using only one static restriction. 
Given an instance of PCP we build a set of
processes $P_1,\dots,P_n$, one for each tile $T_1,\dots,T_n$, and show
that, for each $i$, $P_i$ is bisimilar to $\encp{!\nil}{!}$ iff the instance of
PCP has no solution ending with $T_i$. Thus PCP is solvable iff there
exists $j$ such that $P_j$ is not bisimilar to $\encp{!\nil}{!}$.

% Let us define $P_{\tau}=\nu a\ !(a.\nil \parallel \co{a})$. This process
% has only infinite computations with all labels equal to $\tau$. Notice
% also that this behavior can be encoded in \ahopi with two top-level
% restrictions, one for replication and one for $a$ (actually,
% one restriction is enough: the encoding of $!0$ is bisimilar to the
% encoding of $!\tau$).  Given an instance of PCP we build a set of
% processes $P_1,\dots,P_n$, one for each tile $T_1,\dots,T_n$, and show
% that, for each $i$, $P_i$ is bisimilar to $P_{\tau}$ iff the instance of
% PCP has no solution ending with $T_i$. Thus PCP is solvable iff there
% exists $j$ such that $P_j$ is not bisimilar to $P_{\tau}$.

%\finish{ eliminare occorrenze di $P_{\tau}$ }
 

The processes $P_1,\dots,P_n$
execute
in two distinct phases: first they build a possible
solution of PCP, then they non-deterministically stop
building the solution and execute it. If the chosen composition is a
solution then a signal on a free channel $success$ is sent, thus
performing a visible action, which breaks bisimilarity with $\encp{!\nil}{!}$.
%$P_{\tau}$.

The precise encoding of PCP into \ahopi is shown in Figure
\ref{t:encod-pcp}, and described below.  We consider an alphabet of two letters, $a_1$ and $a_2$.  
%The idea is to treat the upper and lower words
%of a tile separately,
%and encode each letter as a process whose continuation encodes the
%rest of the string. 
%The idea is to treat t
The upper and lower words
of a tile are treated as separate {\em strings}, which are 
encoded letter by letter.
The encoding of a letter is then a process whose continuation encodes the
rest of the string, and varies depending on whether the
letter occurs in the upper or in the lower word.  
We use a single channel %$a$ 
to encode both letters:
for the upper word, 
$a_1$ is encoded as $\out a P$ and $a_2$ as $a(x).(x \parallel P)$, where $P$ is the continuation and $x$ does not occur in $P$; 
for the lower word the
encodings are switched.
%For the upper word, 
%$a_1$ is encoded as $\co{a}.P$ and $a_2$ as $a.P$ for
%some channel $a$, where $P$ is the continuation; encodings are
%switched in the lower word. 
In Figure \ref{t:encod-pcp},
$\encl{a_i}{P}{w}$ denotes the encoding of the letter $a_i$ with continuation
$P$, with $w=u$ if the encoding is on the upper word,
$w=l$ otherwise. 
Hence, 
given a string $s = a_i \cdot s'$, 
its encoding $\encs{s}{P}{w}$ is $\encl{a_i}{\encs{s'}{P}{w}}{w}$, 
i.e., the first letter with the encoding of the rest as continuation.
Notice that
%in this way, 
the encoding of an $a_i$ in the upper word 
can synchronize only with the encoding of $a_i$ for the lower word.
%and that for the lower word 
%two encodings of $a_1$ on the upper and lower words respectively, 
%can synchronize. %, and the same for $a_2$.
%Encodings of letters and strings are given in Table \ref{t:encod-pcp}:
%function $\encl{a_i}{P}{w}$ encodes letter $a_i$ with continuation
%$P$, with $w=u$ if the encoding is on the upper word,
%$w=l$ otherwise. 
%Hence, the encoding of a string $\encs{s}{P}{w}$ is the encoding of
%the first letter with the encoding of the rest as continuation.


\begin{figure}[t]  
\centering  
%{\small  
\begin{tabular}{l} 
		\(   
		\begin{array}{ll}   
		\mathrm{\textsc{Letters}}&  \encl{a_1}{P}{u}=\encl{a_2}{P}{l}=\co{a}\angp{P} \\
		&  \encl{a_2}{P}{u}=\encl{a_1}{P}{l}=a(x).(x \parallel P) \\
		\mathrm{\textsc{Strings}}&  \encs{a_i \cdot s}{P}{w}=\encl{a_i}{\encs{s}{P}{w}}{w}  \\
                &  \encs{\epsilon}{P}{w}=P \qquad \textrm{($\epsilon$ is the empty word)}\\ 
                \iflong{
		\mathrm{\textsc{Creators}}  & C_k=up(x).low(y).(\co{up}\angp{\encs{u_k}{x}{u}} \parallel \co{low}\angp{\encs{l_k}{y}{l}}) \\
                }{
                \mathrm{\textsc{Creators}}  & C_k=up(x).low(y). \\
		& \qquad \qquad \qquad (\co{up}\angp{\encs{u_k}{x}{u}} \parallel \co{low}\angp{\encs{l_k}{y}{l}}) \\
                                }   
		\mathrm{\textsc{Starters}}  & S_k=\co{up}\angp{\encs{u_k}{\co{b}}{u}} \parallel \co{low}\angp{\encs{l_k}{b.\co{success}}{l}} \\
		\mathrm{\textsc{Executor}}~  & E=up(x).low(y).(x \parallel y) \\
		\mathrm{\textsc{System}} &  P_j = \res{ up}\res{low}\res a\res{b } (\ S_j \parallel !\prod_k C_k \parallel E)
		\end{array}
\)
\end{tabular}
%}
\caption{Encoding of PCP into \ahopi}  
\label{t:encod-pcp}  
\end{figure}



%\begin{mydefi}
%$$\encl{a_1}{P}{u}=\encl{a_2}{P}{l}=\co{a}\angp{P}$$
%$$\encl{a_2}{P}{u}=\encl{a_1}{P}{l}=a(x).(x \parallel P)$$ 
%Similarly, t
%\end{mydefi}
%\noindent 

The whole system $P_j$ is composed by a (replicated) {\em creator} $C_k$ for each tile
$T_k$, a {\em starter} $S_j$ that launches the building of a tile
composition ending with $(u_j,l_j)$, and an {\em executor} $E$.  
The starter makes the computation begin; creators non-deterministically add their tile to
the beginning of the composition. 
Also non-deterministically, the executor blocks the building 
of the composition and starts its execution.
This proceeds if no
difference is found: if both strings end at the same
character, then synchronization on channel $b$ 
can be performed, which in turn, makes % and hence the 
action $\co{success}$ %becomes 
visible.
Notice that without synchronizing on $b$, %the executor could perform
action $\co{success}$ could be visible even %for two strings 
%containing differences.
in the case in which one of the strings is a prefix of the other one.

%of the form:
%$$C_i=up(x).low(y).(\co{up}\angp{\encs{u_i}{x}{u}} \parallel \co{low}\angp{\encs{l_i}{y}{l}})$$
%$$S_{u,l}=\co{up}\angp{\encs{u}{\co{b}}{u}} \parallel \co{low}\angp{\encs{l}{b.\co{success}}{l}}$$
%for some strings $u$ and $l$. Name $b$ is used when the two
%strings are executed to check whether they are equal. If so, 
%
%We denote with $E$ the process that 
%$$E=up(x).low(y).(x \parallel y)$$
%The complete system is given by $P_j$. It 
%$$P_j = \res{ up}\res{low}\res a\res{b } (\ S_{u_j,l_j} \parallel !\prod_i C_i \parallel E)$$
%This system 
%non-deterministically creates any tile composition ending
%with $T_j$ and executes it. The upper and lower parts can synchronize
%only if they are equal, thus executing action $\co{success}$.

The encoding of replication requires another restriction, thus $P_j$
has five restrictions. However, names $low$ and $a$ are used in
different phases; thus choosing $low=a$ does not create interferences,
and four restrictions are enough.

\begin{mytheo}\label{th:PCP}
Given an instance of PCP and one of its tiles $T_j$, 
there is a solution of the instance of PCP ending with $T_j$
%$P_{\tau}$ 
iff $P_j$ is not bisimilar to $\encp{!\nil}{!}$ 
according to any complete $\tau$-bisimilarity.
\end{mytheo}
\iflong{
\begin{proof}
We start by proving the left to right implication. 
Note that $\encp{! \nil}{!}$ has a unique possible computation, that is infinite and includes only $\tau$ actions.
Let $T_{i_1}, \ldots, T_{i_m}$ be a solution of the instance of the PCP problem such that $T_{i_m} = T_j$.
Then $P_j$ can perform the computation described below, which contains the action  $\co{success}$, thus 
it is not bisimilar to  $\encp{! \nil}{!}$.
The computation is as follows: 
\begin{enumerate}
\item $P_j \arr \tau^* \nu up,a,b. \, S_j \parallel \prod_{h = 1..m-1} C_{i_h} \parallel \prod C \parallel !\,\prod_{k} C_{k} \parallel E \label{eq:iter} = P'_1$, by replication unfolding (the $\prod C$ is the parallel composition of the creators that have been replicated and will not be used);
\item $P'_1 \arr \tau^* \nu up,a,b. \,\co{up}\angp{\encs{u}{\co{b}}{u}} \parallel \co{a}\angp{\encs{l}{b.\co{success}}{l}} \parallel \prod C \parallel !\,\prod_{k} C_{k} \parallel E = P'_2$, where $(u,l)$ is the solution of the instance of the PCP problem, by making the starter $S_j$ interact with the creators $C_{i_{m-1}}..C_{i_1}$;
\item $P'_2 \arr \tau \arr \tau \nu up,a,b. \, \prod C \parallel !\,\prod_k C_k
\parallel \encs{u}{\co{b}}{u} \parallel \encs{l}{b.\co{success}}{l} = P'_3$, by making the starter interact with the executor (note that as every creator starts by an input on $up$, none of them my be triggered by messages on $\co{a}$);
\item $P'_3 \arr \tau^* \nu up,a,b. \, \prod C \parallel !\,\prod_k C_k 
\parallel\co{b} \parallel b.\co{success} = P'_4$, by executing the encodings of the two strings, exploiting the fact that they are equal;
\item $P'_4 \arr \tau \nu up,a,b. \, \prod C \parallel !\,\prod_k C_k \parallel \co{success} = P'_5$, by synchronizing on $b$;
\item $P'_5  \arr {\co{success}} \nu up,a,b. \, \prod C \parallel !\,\prod_k C_k$.
\end{enumerate} 

For the other implication, first notice that all the computations of $P_j$ are infinite since one can always unfold recursion, and
action $\co{success}$ is the only possible visible action. 
Thus the only possibility for having $P_j$ not bisimilar to  $\encp{! \nil}{!}$ is that $P_j$ has a computation executing 
$\co{success}$. The only computations that may produce $\co{success}$ are structured as follows: they build two strings by concatenating the tiles, and then they execute them. One can prove by induction on the minimum length of the strings that if the two strings are different then either their execution gets stuck, or synchronization at $b$ is not possible (this last case occurs if one of the strings is a prefix of the other). Thus, the two strings must be equal and they are the solution of the instance of the PCP problem.
\end{proof}
}
{
\begin{proof}[Proof (Sketch)]
%The proof starts by 
Note that all computations are infinite, and
the only possible observable action is $\co{success}$. One can show
that for each $n \geq 1$ and each tile composition $(u_1 \cdots
u_n,l_1\cdots l_n)$ with $T_j=(u_n,l_n)$ there is a computation whose
transitions have label $\tau$ leading to:
\begin{equation}\label{eq:end}
\begin{array}{rcl}
P'_{m'} & = & \nu up,low,a,b. \ \ !\prod_i C_i \parallel \prod_{k} C_{i_k}
\parallel \\
& & \encs{u_1 \cdots u_n}{\co{b}}{u} \parallel
\encs{l_1\cdots l_n}{b.\co{success}}{l}
\end{array}
\end{equation}
where $i_k$ are values in $\{1,\dots,n\}$ (not necessarily distinct).
The proof is concluded by showing that each process of the form above
has a computation containing an output at ${success}$ iff $u_1 \cdots
u_n=l_1\cdots l_n$.
\end{proof}
}


\begin{mycoro}
Barbed congruence and any complete $\tau$-bisimilarity are undecidable in \ahopi with four static restrictions.
\end{mycoro}


Theorem~\ref{th:PCP} actually shows that  even \emph{asynchronous barbed
bisimilarity} (defined as the largest $\tau$-bisimilarity that is output-barb
preserving, and  used in the definition of ordinary---as
opposed to reduction-closed---barbed congruence)
is undecidable. The corollary above then follows from the fact that
all the relations there mentioned are at least as demanding as asynchronous barbed
bisimilarity. 

% \begin{mycoro}
% All complete $\tau$-bisimilarities are undecidable in \ahopi with four static restrictions.
% \end{mycoro}

% \begin{mycoro}
% Barbed congruence is undecidable in \ahopi with four static restrictions.
% \end{mycoro}
